Confirming that a circuit design satisfies the specified requirements is the basis of verification processes. One main aspect of the verification process includes specification. Conventional specification practices include creating a natural language description of a circuit's design requirements. However, the natural language description lacks a machine-executable representation, which is usually vague and in many cases unverifiable. In addition, in recent years, the demand for formal specification languages is growing as more and more engines capable of handling formal verification languages become available in verification environments. All the advances require a more sophisticated property specification language.
PSL is an Accellera Standard language for property specification. It is used for specifying hardware design behavior and interface requirements. The PSL specification can be used in simulation, emulation, and model checking (formal) verification engines to check the hardware design.
The language PSL, supports linear temporal logic (LTL) and computational tree logic (CTL) formulas. It has unique regular expression based formula called SERE (Sugar Extended Regular Expressions) implication. The LTL and SERE forms together are called foundation language (FL) formulas. The language defines subset of FL, which can also be verified using simulation. This subset is called ‘simple-subset’ of PSL. The disclosure presents a novel method to support ‘simple-subset’ of PSL by simulation and model checking.
Buchi Automata is a well-studied form of automata to represent LTL formulas in LTL model checking. The LTL formulas are converted to Buchi Automata. The standard model checking consists of taking cross product of model (design automaton) and Buchi automation of the complement of LTL formula. The cross product is checked for empty language. The Buchi automata could have O(2n) states in worst-case where n is the size of LTL formula. The size of Buchi automation, and hence the quality of LTL formula transformation, is very important for efficiency of model checking. This process is shown in FIG. 2A and described further below.
Formula in ‘simple-subset’ of PSL can be transformed to a set of SERE implication formulas with optional ‘abort’. This disclosure describes a method to show that SERE implication support is powerful enough to support ‘simple-subset’ of PSL.
Efficiency of automata construction is addressed by two approaches. Handcrafted parameterized automation modules are constructed for generic SEREs. These are specific to modeling checking and simulation engines. In addition, transformation rules have been developed to optimize SEREs before implementing it with automatons for simulation and model checking.